(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 15))
(let ((e3 14))
(let ((e4 4))
(let ((e5 (* v1 e2)))
(let ((e6 (- v1)))
(let ((e7 (- v0)))
(let ((e8 (+ e6 e6)))
(let ((e9 (- e7)))
(let ((e10 (- v0 e6)))
(let ((e11 (* v0 v1)))
(let ((e12 (- e5)))
(let ((e13 (- e11 v0)))
(let ((e14 (/ e4 e2)))
(let ((e15 (- e6 e7)))
(let ((e16 (- e11)))
(let ((e17 (- e8 e5)))
(let ((e18 (+ e13 e12)))
(let ((e19 (- e8 e18)))
(let ((e20 (+ e8 e13)))
(let ((e21 (- v1)))
(let ((e22 (/ e3 (- e2))))
(let ((e23 (distinct e11 e9)))
(let ((e24 (distinct e9 e13)))
(let ((e25 (< e12 e20)))
(let ((e26 (<= e21 e18)))
(let ((e27 (= e8 e19)))
(let ((e28 (> e7 e20)))
(let ((e29 (distinct e17 e22)))
(let ((e30 (> e14 e12)))
(let ((e31 (= e12 e11)))
(let ((e32 (distinct e9 e10)))
(let ((e33 (= e21 e12)))
(let ((e34 (distinct e12 e6)))
(let ((e35 (= e16 e12)))
(let ((e36 (<= e9 e17)))
(let ((e37 (distinct e14 e7)))
(let ((e38 (>= e18 e21)))
(let ((e39 (> e17 e10)))
(let ((e40 (< e21 e18)))
(let ((e41 (distinct e10 e12)))
(let ((e42 (> e7 e9)))
(let ((e43 (>= e19 v1)))
(let ((e44 (> e19 e11)))
(let ((e45 (distinct e19 e20)))
(let ((e46 (distinct e6 e5)))
(let ((e47 (> v1 e10)))
(let ((e48 (= e5 e12)))
(let ((e49 (distinct e10 e6)))
(let ((e50 (> e11 e11)))
(let ((e51 (distinct e15 e20)))
(let ((e52 (= v1 e7)))
(let ((e53 (> e12 e20)))
(let ((e54 (< e21 e5)))
(let ((e55 (>= e10 e16)))
(let ((e56 (> e7 e10)))
(let ((e57 (distinct e10 e10)))
(let ((e58 (= v1 e18)))
(let ((e59 (>= e9 e8)))
(let ((e60 (>= e9 e8)))
(let ((e61 (> e20 e15)))
(let ((e62 (< e13 e12)))
(let ((e63 (<= e8 e11)))
(let ((e64 (>= e7 v1)))
(let ((e65 (< e11 e9)))
(let ((e66 (= e5 e7)))
(let ((e67 (< e17 e15)))
(let ((e68 (distinct e13 e18)))
(let ((e69 (< e14 e12)))
(let ((e70 (= e18 e15)))
(let ((e71 (>= e15 e11)))
(let ((e72 (distinct e8 e7)))
(let ((e73 (<= v0 e14)))
(let ((e74 (< e5 e11)))
(let ((e75 (distinct e15 v0)))
(let ((e76 (< e9 e15)))
(let ((e77 (>= e6 e7)))
(let ((e78 (>= e17 e21)))
(let ((e79 (<= e10 e13)))
(let ((e80 (distinct e14 e19)))
(let ((e81 (< e13 e16)))
(let ((e82 (>= e6 e7)))
(let ((e83 (> e19 e7)))
(let ((e84 (= e9 e18)))
(let ((e85 (distinct e11 e10)))
(let ((e86 (distinct e7 e16)))
(let ((e87 (distinct e19 e7)))
(let ((e88 (distinct e14 e18)))
(let ((e89 (= e12 e9)))
(let ((e90 (>= e5 e17)))
(let ((e91 (<= e14 e7)))
(let ((e92 (distinct e10 e16)))
(let ((e93 (< e15 e22)))
(let ((e94 (distinct e16 e19)))
(let ((e95 (> e21 e7)))
(let ((e96 (distinct e18 e19)))
(let ((e97 (> e8 e19)))
(let ((e98 (<= e20 e5)))
(let ((e99 (> e6 e17)))
(let ((e100 (distinct e6 e14)))
(let ((e101 (distinct e19 e6)))
(let ((e102 (< e21 e7)))
(let ((e103 (= e17 e12)))
(let ((e104 (distinct e18 e21)))
(let ((e105 (= e14 e5)))
(let ((e106 (<= e5 e9)))
(let ((e107 (= e18 e20)))
(let ((e108 (<= e8 e22)))
(let ((e109 (= e7 e21)))
(let ((e110 (>= e11 e7)))
(let ((e111 (= v0 e22)))
(let ((e112 (> e13 e22)))
(let ((e113 (<= e14 e13)))
(let ((e114 (<= e17 e14)))
(let ((e115 (<= e8 e12)))
(let ((e116 (>= e22 e18)))
(let ((e117 (<= e10 e19)))
(let ((e118 (<= e10 v1)))
(let ((e119 (or e36 e45)))
(let ((e120 (=> e85 e43)))
(let ((e121 (ite e59 e67 e37)))
(let ((e122 (= e105 e71)))
(let ((e123 (= e41 e94)))
(let ((e124 (or e103 e101)))
(let ((e125 (= e50 e117)))
(let ((e126 (ite e84 e115 e116)))
(let ((e127 (not e54)))
(let ((e128 (and e31 e91)))
(let ((e129 (not e112)))
(let ((e130 (= e49 e107)))
(let ((e131 (xor e27 e44)))
(let ((e132 (=> e35 e92)))
(let ((e133 (ite e99 e68 e118)))
(let ((e134 (and e130 e77)))
(let ((e135 (=> e23 e124)))
(let ((e136 (xor e52 e38)))
(let ((e137 (xor e135 e83)))
(let ((e138 (and e66 e53)))
(let ((e139 (and e51 e79)))
(let ((e140 (=> e89 e136)))
(let ((e141 (ite e63 e95 e32)))
(let ((e142 (=> e122 e39)))
(let ((e143 (=> e62 e56)))
(let ((e144 (or e30 e96)))
(let ((e145 (not e133)))
(let ((e146 (and e28 e111)))
(let ((e147 (or e102 e55)))
(let ((e148 (=> e137 e74)))
(let ((e149 (=> e106 e147)))
(let ((e150 (ite e81 e142 e47)))
(let ((e151 (not e26)))
(let ((e152 (xor e104 e149)))
(let ((e153 (= e140 e129)))
(let ((e154 (xor e120 e48)))
(let ((e155 (=> e76 e57)))
(let ((e156 (xor e146 e127)))
(let ((e157 (xor e58 e24)))
(let ((e158 (and e78 e145)))
(let ((e159 (=> e157 e108)))
(let ((e160 (and e132 e69)))
(let ((e161 (= e123 e125)))
(let ((e162 (not e144)))
(let ((e163 (=> e64 e152)))
(let ((e164 (=> e42 e40)))
(let ((e165 (xor e114 e159)))
(let ((e166 (or e110 e163)))
(let ((e167 (and e154 e153)))
(let ((e168 (ite e29 e88 e82)))
(let ((e169 (ite e160 e126 e113)))
(let ((e170 (not e158)))
(let ((e171 (ite e162 e121 e60)))
(let ((e172 (ite e97 e33 e119)))
(let ((e173 (xor e172 e46)))
(let ((e174 (not e169)))
(let ((e175 (not e34)))
(let ((e176 (= e150 e161)))
(let ((e177 (or e171 e75)))
(let ((e178 (=> e175 e90)))
(let ((e179 (= e167 e177)))
(let ((e180 (xor e73 e70)))
(let ((e181 (ite e148 e109 e87)))
(let ((e182 (and e165 e180)))
(let ((e183 (and e131 e179)))
(let ((e184 (xor e25 e174)))
(let ((e185 (= e65 e61)))
(let ((e186 (ite e170 e151 e151)))
(let ((e187 (= e100 e166)))
(let ((e188 (xor e80 e183)))
(let ((e189 (xor e86 e168)))
(let ((e190 (not e182)))
(let ((e191 (not e141)))
(let ((e192 (xor e176 e72)))
(let ((e193 (ite e156 e164 e139)))
(let ((e194 (= e186 e134)))
(let ((e195 (and e188 e193)))
(let ((e196 (=> e184 e178)))
(let ((e197 (=> e128 e192)))
(let ((e198 (not e181)))
(let ((e199 (=> e143 e187)))
(let ((e200 (xor e93 e98)))
(let ((e201 (not e138)))
(let ((e202 (and e195 e195)))
(let ((e203 (not e155)))
(let ((e204 (and e200 e189)))
(let ((e205 (and e201 e194)))
(let ((e206 (xor e205 e199)))
(let ((e207 (and e206 e204)))
(let ((e208 (not e197)))
(let ((e209 (or e203 e196)))
(let ((e210 (xor e190 e191)))
(let ((e211 (and e210 e173)))
(let ((e212 (and e198 e211)))
(let ((e213 (= e202 e209)))
(let ((e214 (xor e213 e185)))
(let ((e215 (= e207 e208)))
(let ((e216 (not e212)))
(let ((e217 (and e216 e215)))
(let ((e218 (or e214 e214)))
(let ((e219 (or e217 e217)))
(let ((e220 (not e218)))
(let ((e221 (and e220 e220)))
(let ((e222 (or e221 e221)))
(let ((e223 (not e219)))
(let ((e224 (and e223 e222)))
e224
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
